$\forall$$T$,$X$:Type, ${\it eq}$:EqDecider($X$), $f$,$g$:fpf($X$; $x$.Type), $x$:$X$.
\\[0ex]fpf{-}sub($X$; $x$.Type; ${\it eq}$; $f$; $g$) $\Rightarrow$ subtype\_rel(fpf{-}cap($f$; ${\it eq}$; $x$; void); fpf{-}cap($g$; ${\it eq}$; $x$; $T$))